| Definitions |  x:A. B(x), t  T,   x. t(x), Prop, P   Q, P  Q, ecl-es-halt(es;x), ecl-halt(ds;da;x), P & Q, P Q, if b t else f fi, true, false, SQType(T), {T}, Valtype(da;k), Top, es-hist{i:l}(es;e1;e2), A & B,  x:A. B(x), State(ds), event-info(ds;da), let x,y,z = a in t(x;y;z), state@i, xL. P(x),  A, False, es-info(es;e), map(f;as), Y, S  T, e2 = first e  e1.P(e),  b, last(L), null(as), l[i], ||as||, hd(l), nth_tl(n;as), i j, b, i<j, as @ bs,  T, True, e[e1,e2).P(e), e[e1,e2].P(e), P  Q,  , AB, e(e1,e2].P(e), e[e1,e2].P(e), e e' , [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), star-append(T;P;Q), x,y. t(x;y), {i..j }, i j < k, concat(ll), upto(n), i=j, reduce(f;k;as), S  T, x(s),  , Unit, Dec(P), (e <loc e'), 1of(t), 2of(t), Trans x,y:T. E(x;y), x(s1,s2),  ,  |
| Lemmas | ecl-induction, fpf wf, Knd wf, Id wf, iff wf, ecl-es-halt wf, es-hist wf, es-loc wf, bool cases, eq int wf, bool sq, bool wf, iff transitivity, assert wf, eqtt to assert, assert of eq int, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, nat wf, es-E wf, es-valtype wf, ma-valtype wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, event system wf, decl-state wf, last lemma, event-info wf, null wf3, es-locl wf, null-es-hist, map wf, es-interval wf, es-le-not-locl, Kind-deq wf, append wf, l all wf, last-es-hist, es-state-when wf, subtype rel dep function, subtype rel self, es-val wf, Knd sq, l member wf, es-hist-is-append, decidable false, nil member, length wf1, member-es-hist, es-pred wf, es-locl-iff, es-le-loc, es-loc-pred, es-le-trans3, es-le-pred, decidable es-le, es-interval-is-nil, decidable es-locl, length-append, non neg length, last append, false wf, last wf, pi2 wf, pi1 wf, squash wf, true wf, es-le wf, es-info wf, es-hist-partition, es-le-self, es-le-trans2, general-append-cancellation, es-interval-eq, ecl-halt wf, eclseq wf, subtype rel wf, le wf, existse-between3 wf, es-first wf, ecl-halt-nil, ecland wf, iseg wf, es-hist-iseg, iseg-es-hist, ecl-ex wf, nat plus inc, nat plus wf, l-all-iff, le int wf, assert of le int, alle-between1 wf, lt int wf, bnot of le int, assert of lt int, alle-between2 wf, ecl-halt-ex, es-le-iff, existse-between2 wf, es-hist-one-one, es-le-trans, es-locl-antireflexive, l-all wf, eclor wf, ifthenelse wf, es-pstar-q wf, star-append wf, eclrepeat wf, int seg wf, upto wf, member map, nat plus properties, decidable int equal, map append sq, concat append, append assoc sq, concat wf, append-nil, decidable assert, assert of null, es-hist-is-concat, Id sq, select member, eclact wf, eclthrow wf, l exists wf, eclcatch wf |
Type, da:k:Knd fp
ds(x)?Top)
